#include <Nanobdd.h>
#include <Prime.h>
#include <execution>
#include <future>

/**
 * Dev notes:
 * 1. We must have node cache "level, left, right". When cache not hit, a new
 * bdd node will be made, there will be multiple bdd nodes for the same
 * expression, and the == operator will not work in this case.
 */
namespace nanobdd {

Nanobdd::Nanobdd(size_t tableSize, size_t bucketSize, size_t cacheSize)
    : nodeTable_(bdd_prime_gte(tableSize), bucketSize),
      cacheSize_(bdd_prime_gte(cacheSize)),
      cache_(bdd_prime_gte(cacheSize)) {
  // cache_.resize(cacheSize);

  // Be aware the position of const nodes in nodeTable
  Nanobdd::falseNode = makeNode(32, nullptr, nullptr);

  Nanobdd::trueNode = makeNode(33, nullptr, nullptr);
}

void
Nanobdd::createVars(int num) {
  for (int i = 0; i < num; ++i) {
    createVar(i);
  }
}

Bdd&
Nanobdd::createVar(int id) {
  auto node = makeNode(id, falseNode, trueNode);
  vars_.emplace(vars_.begin() + id, node);
  auto nvar = makeNode(id, trueNode, falseNode);
  nvars_.emplace(nvars_.begin() + id, nvar);
  return vars_.at(id);
}

Bdd&
Nanobdd::getVar(int id) {
  return vars_.at(id);
}

Bdd&
Nanobdd::getNvar(int id) {
  return nvars_.at(id);
}

Node*
Nanobdd::makeNode(int level, Node* low, Node* high) {
  return (nodeTable_(level, low, high));
}

Bdd
Nanobdd::bddAnd(const Bdd& x, const Bdd& y) {
  if (x == y) {
    return x;
  }
  if (x.isFalse() || y.isFalse()) {
    return Nanobdd::falseNode;
  }
  if (x.isTrue()) {
    return y;
  }
  if (y.isTrue()) {
    return x;
  }
  int m = std::min(x.level(), y.level());

  auto hash = HASH_UO_O_3(
                  reinterpret_cast<uintptr_t>(x.node()),
                  reinterpret_cast<uintptr_t>(y.node()),
                  0) %
      cacheSize_;
  auto cached = cache_.lookup(hash, x.node(), y.node(), 0);
  if (cached) {
    return cached;
  }

  // std::vector<int> t{0, 1};
  // Bdd fLow, fHigh;
  // std::for_each(std::execution::par, t.begin(), t.end(), [&](int v){
  //   if (v == 0) {
  //     fLow =  bddAnd(negCof(x, m), negCof(y, m));
  //   } else {
  //     fHigh = bddAnd(posCof(x, m), posCof(y, m));
  //   }
  // });

  // std::future<Bdd> rLow =
  //     std::async([&]() { return bddAnd(negCof(x, m), negCof(y, m)); });
  // std::future<Bdd> rHigh =
  //     std::async([&]() { return bddAnd(posCof(x, m), posCof(y, m)); });
  // auto fLow = rLow.get();
  // auto fHigh = rHigh.get();

  auto fLow = bddAnd(negCof(x, m), negCof(y, m));
  auto fHigh = bddAnd(posCof(x, m), posCof(y, m));

  auto res = combine(m, fLow, fHigh);

  cache_.insert(hash, res, x.node(), y.node(), 0);

  return res;
}

Bdd
Nanobdd::bddOr(const Bdd& x, const Bdd& y) {
  if (x.node() == y.node()) {
    return x;
  }
  if (x.isTrue() || y.isTrue()) {
    return Nanobdd::trueNode;
  }
  if (x.isFalse()) {
    return y;
  }
  if (y.isFalse()) {
    return x;
  }
  int m = std::min(x.level(), y.level());

  auto hash = HASH_UO_O_3(
                  reinterpret_cast<uintptr_t>(x.node()),
                  reinterpret_cast<uintptr_t>(y.node()),
                  1) %
      Nanobdd::cacheSize_;
  auto cached = cache_.lookup(hash, x.node(), y.node(), 1);
  if (cached) {
    return cached;
  }

  // std::vector<int> t{0, 1};
  // Bdd fLow, fHigh;
  // std::for_each(std::execution::par, t.begin(), t.end(), [&](int v){
  //   if (v == 0) {
  //     fLow =  bddOr(negCof(x, m), negCof(y, m));
  //   } else {
  //     fHigh = bddOr(posCof(x, m), posCof(y, m));
  //   }
  // });

  // std::future<Bdd> rLow =
  //     std::async([&]() { return bddOr(negCof(x, m), negCof(y, m)); });
  // std::future<Bdd> rHigh =
  //     std::async([&]() { return bddOr(posCof(x, m), posCof(y, m)); });
  // auto fLow = rLow.get();
  // auto fHigh = rHigh.get();

  auto fLow = bddOr(negCof(x, m), negCof(y, m));
  auto fHigh = bddOr(posCof(x, m), posCof(y, m));

  auto res = combine(m, fLow, fHigh);

  cache_.insert(hash, res, x.node(), y.node(), 1);

  return res;
}

Bdd
Nanobdd::bddDiff(const Bdd& x, const Bdd& y) {
  if (x.node() == y.node() || x.isFalse() || y.isTrue()) {
    return Nanobdd::falseNode;
  }
  if (y.isFalse()) {
    return x;
  }

  int m = std::min(x.level(), y.level());

  auto hash = HASH_UO_O_3(
                  reinterpret_cast<uintptr_t>(x.node()),
                  reinterpret_cast<uintptr_t>(y.node()),
                  3) %
      Nanobdd::cacheSize_;
  auto cached = cache_.lookup(hash, x.node(), y.node(), 3);
  if (cached) {
    return cached;
  }

  // std::vector<int> t{0, 1};
  // Bdd fLow, fHigh;
  // std::for_each(std::execution::par, t.begin(), t.end(), [&](int v){
  //   if (v == 0) {
  //     fLow =  bddDiff(negCof(x, m), negCof(y, m));
  //   } else {
  //     fHigh = bddDiff(posCof(x, m), posCof(y, m));
  //   }
  // });

  // std::future<Bdd> rLow =
  //     std::async([&]() { return bddDiff(negCof(x, m), negCof(y, m)); });
  // std::future<Bdd> rHigh =
  //     std::async([&]() { return bddDiff(posCof(x, m), posCof(y, m)); });
  // auto fLow = rLow.get();
  // auto fHigh = rHigh.get();

  auto fLow = bddDiff(negCof(x, m), negCof(y, m));
  auto fHigh = bddDiff(posCof(x, m), posCof(y, m));

  auto res = combine(m, fLow, fHigh);

  cache_.insert(hash, res, x.node(), y.node(), 3);

  return res;
}

Bdd
Nanobdd::bddNot(const Bdd& x) {
  if (x.isTrue()) {
    return Nanobdd::falseNode;
  }
  if (x.isFalse()) {
    return Nanobdd::trueNode;
  }

  // auto hash = TRIPLEp(x.node(), nullptr, 2) % Nanobdd::cacheSize_;
  auto hash =
      HASH_UO_O_3(reinterpret_cast<uintptr_t>(x.node()), 0, 2) % cacheSize_;
  auto cached = cache_.lookup(hash, x.node(), nullptr, 2);
  if (cached) {
    return cached;
  }

  int m = x.level();

  // std::vector<int> t{0, 1};
  // Bdd fLow, fHigh;
  // std::for_each(std::execution::par, t.begin(), t.end(), [&](int v){
  //   if (v == 0) {
  //     fLow =  bddNot(negCof(x, m));
  //   } else {
  //     fHigh = bddNot(posCof(x, m));
  //   }
  // });

  // std::future<Bdd> rLow =
  //     std::async([&]() { return bddNot(negCof(x, m)); });
  // std::future<Bdd> rHigh =
  //     std::async([&]() { return bddNot(posCof(x, m)); });
  // auto fLow = rLow.get();
  // auto fHigh = rHigh.get();

  auto fLow = bddNot(negCof(x, m));
  auto fHigh = bddNot(posCof(x, m));

  auto res = combine(m, fLow, fHigh);

  cache_.insert(hash, res, x.node(), nullptr, 2);

  return res;
}

Bdd
Nanobdd::negCof(const Bdd& x, int id) const {
  // check id <= root_
  if (id < x.level()) {
    return x;
  } else { // id == root_
    return x.node()->low;
  }
}

Bdd
Nanobdd::posCof(const Bdd& x, int id) const {
  // check id <= root_
  if (id < x.level()) {
    return x;
  } else { // id == root_
    return x.node()->high;
  }
}

Node*
Nanobdd::combine(size_t level, const Bdd& low, Bdd& high) {
  if (low == high) {
    return low.node();
  }
  return makeNode(level, low.node(), high.node());
}

} // namespace nanobdd